MIME-Version: 1.0
Server: CERN/3.0
Date: Wednesday, 20-Nov-96 19:50:12 GMT
Content-Type: text/html
Content-Length: 1637
Last-Modified: Thursday, 02-May-96 20:57:32 GMT

<html>
<head>
<title>Ashvin M Dsouza
</title>
<h1> 
Ashvin Dsouza <img src="ashvin.gif">  
</h1>
<p>
<em>dsouza@cs.cornell.edu</em>
</head>
<body>
<rm>
<p>
I'm a graduate student working with Bard Bloom.
The focus of my thesis research is the development of
tools to support process algebraic methods for the specification and
verification of concurrent systems. By designing these tools with
respect to a metatheory of process algebras, they become immediately
available to a wide class of process algebras. This alleviates the
problem of duplicated effort inherent in custom tools.  For example,
I have designed and prototyped a BDD-based mu-calculus model checker 
for simple GSOS process algebras. The semantics of the process algebra 
forms part of the input, making this tool applicable to many commonly 
used process algebras, including CCS, CSP and basic LOTOS. In addition, 
I am investigating the expressive power of process algebras in order 
to better understand and compare them. Finally, I am exploring
applications of these techniques.
</rm>
<p>
Here's some work on generating BDDs for process algebra
terms, in full
(<A HREF="./pa2bdd.ps"> postscipt </A>) 
and lite 
(<A HREF="./pa2bdd-lite.ps"> postscript </A>) versions.
I've also written up some expressiveness results for CCS 
(<A HREF="./ccs.ps"> postscript </A>). I have presented
the former at <i> Computer Aided Verification 95 </i>
(LNCS 939), and the latter at 
<i>
Foundations of Software Technology and Theoretical Computer
Science </i> (LNCS 1026). This June, I will be presenting 
work on verifying SOS specifications at <i>COMPASS '96</i>.
</body>
</html>
